es:ES, e:E, x:Id. state when e\\x  state@loc(e)\\x 

latex

Definitions	t  T, x:A. B(x), x when e, Id, s = t, , b, Type, A, b, , Void, x:A.B(x), Top, a = b, x:AB(x), P  Q, x:A  B(x), P & Q, P  Q, Unit, left + right, x.A(x), state when e\\x, state@i\\x, ES, E
Lemmas	es-E wf, event system wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, assert wf, Id wf, es-when wf